Nuprl Lemma : length-map
11,40
postcript
pdf
f
:top,
T
:Type,
L
:(
T
List). sqequal(||map(
f
;
L
)||; ||
L
||)
latex
Definitions
x
:
A
.
B
(
x
)
,
||
as
||
,
map(
f
;
as
)
,
Y
,
t
T
Lemmas
top
wf
origin
f:top, T:Type, L:(T List). sqequal(||map(f; L)||; ||L||) f:top, T:Type, L:(T List). sqequal(||map(f; L)||; ||L||) x:A. B(x)
T